Nuprl Lemma : kindcase_wf
0,22
postcript
pdf
B
:Type,
k
:Knd,
f
:(Id
B
),
g
:(IdLnk
Id
B
). kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
,
t
) )
B
latex
Definitions
Knd
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
islocal(
k
)
,
act(
k
)
,
lnk(
k
)
,
tag(
k
)
,
x
(
s1
,
s2
)
,
1of(
t
)
,
2of(
t
)
,
Id
,
IdLnk
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
t
T
Lemmas
pi2
wf
,
Id
wf
,
IdLnk
wf
,
pi1
wf
,
Knd
wf
origin
B:Type, k:Knd, f:(Id
B), g:(IdLnkIdB). kindcase(k; a.f(a); l,t.g(l,t) ) 
B B:Type, k:Knd, f:(IdB), g:(IdLnkIdB). kindcase(k; a.f(a); l,t.g(l,t) ) B 
x. t(x)x:A. B(x) T